\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, ${\it es}$:ES, $i$:Id, ${\it LL}$:(event{-}info(${\it ds}$;${\it da}$) List) List, $e_{1}$,\+
\\[0ex]$e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ $i$ \}, $L$:event{-}info(${\it ds}$;${\it da}$) List.
\-\\[0ex]($\forall$$L$$\in$${\it LL}$. $\neg$$L$ $=$ nil)
\\[0ex]$\Rightarrow$ $\neg$$L$ $=$ nil
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ ${\it da}$(kind($e$))?Top)
\\[0ex]$\Rightarrow$ es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$) $=$ (concat(${\it LL}$) @ $L$) $\in$ event{-}info(${\it ds}$;${\it da}$) List
\\[0ex]$\Rightarrow$ (\=$\exists$$f$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it LL}$$\parallel$+1}}$$\rightarrow$\{$e$:E$\mid$ loc($e$) $=$ $i$ \}).\+
\\[0ex]$f$(0) $=$ $e_{1}$ \& $f$($\parallel$${\it LL}$$\parallel$) $\leq$ $e_{2}$ 
\\[0ex]\& ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it LL}$$\parallel$}}$. ($f$($i$) $<$loc $f$($i$+1)))
\\[0ex]\& \=($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it LL}$$\parallel$}}$. es{-}hist\{i:l\}(${\it es}$;$f$($i$);pred($f$($i$+1))) $=$ ${\it LL}$[$i$] $\in$ event{-}info(${\it ds}$;${\it da}$) List)\+
\\[0ex]\& es{-}hist\{i:l\}(${\it es}$;$f$($\parallel$${\it LL}$$\parallel$);$e_{2}$) $=$ $L$)
\-\-
\end{tabbing}